l1, l2:IdLnk. lnk-inv(l1) = lnk-inv(l2)  IdLnk  l1 = l2 

latex

Definitions	SQType(T), P  Q, P & Q, P  Q, P  Q, lnk-inv(l), x:A. B(x), Prop, t  T, IdLnk
Lemmas	IdLnk wf, lnk-inv wf, lnk-inv-inv